MIME-Version: 1.0
Server: CERN/3.0
Date: Sunday, 24-Nov-96 21:26:23 GMT
Content-Type: text/html
Content-Length: 13407
Last-Modified: Wednesday, 13-Dec-95 02:42:30 GMT


<title>Tom Henzinger: Publications</title>
<h2>List of Publications</h2>
<i><!WA0><!WA0><!WA0><!WA0><a href="http://www.cs.cornell.edu/Info/People/tah/tah.html">
Thomas A. Henzinger</a></i>
<h3><a name="reactive_modules">Reactive Modules</a></h3>
<ul>
<li>Rajeev Alur and Thomas A. Henzinger. 
<b>Local liveness for compositional modeling of fair reactive systems.</b>
<i>Proceedings of the 
Seventh International Conference on Computer-aided Verification</i>
(CAV 1995),
Lecture Notes in Computer Science 939,
Springer-Verlag, 1995, pp. 166-179.
<p>
<li>Rajeev Alur and Thomas A. Henzinger.
<b>Finitary fairness.</b>
<i>Proceedings of the 
Ninth Annual IEEE Symposium on Logic in Computer Science</i>
(LICS 1994), pp. 52-61.
<p>
<li>Monika R. Henzinger, Thomas A. Henzinger, and Peter W. Kopke.
<b>Computing simulations on finite and infinite graphs.</b>
<i>Proceedings of the 
36th Annual IEEE Symposium on Foundations of Computer Science</i>
(FOCS 1995),
pp. 453-462.
</ul>
<h3><a name="real-time_logics">Real-time Logics and Timed Transition 
Systems</a></h3>
<ul>
<li>Rajeev Alur and Thomas A. Henzinger.
<b>Time for logic.</b>
<i>SIGACT News</i> 22:6-12, 1991.
<p>
<li>Rajeev Alur and Thomas A. Henzinger.
<b>Logics and models of real time: a survey.</b>
In 
<i>Real Time: Theory in Practice</i>,
Lecture Notes in Computer Science 600,
Springer-Verlag, 1992, pp. 74-106.
<!WA1><!WA1><!WA1><!WA1><a href="http://www.cs.cornell.edu/Info/People/tah/logics_and_models_of_real_time.html">
Abstract.</a>
Ftp
<!WA2><!WA2><!WA2><!WA2><a href="ftp://ftp.cs.cornell.edu/pub/tah/Papers/logics_and_models_of_real_time.ps">
postscript.</a>
<p>
<li>Rajeev Alur and Thomas A. Henzinger.
<b>A really temporal logic.</b>
<i>Journal of the ACM</i> 41:181-204, 1994.
A preliminary version appeared in the 
<i>Proceedings of the 
30th Annual IEEE Symposium on Foundations of Computer Science</i>
(FOCS 1989), pp. 164-169.
<!WA3><!WA3><!WA3><!WA3><a href="http://www.cs.cornell.edu/Info/People/tah/a_really_temporal_logic.html">
Abstract.</a>
Ftp
<!WA4><!WA4><!WA4><!WA4><a href="ftp://ftp.cs.cornell.edu/pub/tah/Papers/a_really_temporal_logic.ps">
postscript.</a>
<p>
<li>Rajeev Alur and Thomas A. Henzinger.
<b>Real-time logics: complexity and expressiveness.</b>
<i>Information and Computation</i> 104:35-77, 1993.
A preliminary version appeared in the 
<i>Proceedings of the 
Fifth Annual IEEE Symposium on Logic in Computer Science</i>
(LICS 1990), pp. 390-401.
<!WA5><!WA5><!WA5><!WA5><a href="http://www.cs.cornell.edu/Info/People/tah/real-time_logics.html">
Abstract.</a>
Ftp
<!WA6><!WA6><!WA6><!WA6><a href="ftp://ftp.cs.cornell.edu/pub/tah/Papers/real-time_logics.ps">
postscript.</a>
<p>
<li>Thomas A. Henzinger.
<b>Half-order modal logic: how to prove real-time properties.</b>
<i>Proceedings of the 
Ninth Annual ACM Symposium on Principles of Distributed Computing</i>
(PODC 1990), pp. 281-296.
<!WA7><!WA7><!WA7><!WA7><a href="http://www.cs.cornell.edu/Info/People/tah/half-order_modal_logic.html">
Abstract.</a>
Ftp
<!WA8><!WA8><!WA8><!WA8><a href="ftp://ftp.cs.cornell.edu/pub/tah/Papers/half-order_modal_logic.ps">
postscript.</a>
<p>
<li>Thomas A. Henzinger, Zohar Manna, and Amir Pnueli.
<b>Temporal proof methodologies for timed transition systems.</b>
<i>Information and Computation</i> 112:273-337, 1994.
Preliminary versions of the two parts appeared, respectively, in the 
<i>Proceedings of the 
18th Annual ACM Symposium on Principles of Programming Languages</i>
(POPL 1991), pp. 353-366, and in
<i>Real Time: Theory in Practice</i>,
Lecture Notes in Computer Science 600,
Springer-Verlag, 1992, pp. 226-251.
<!WA9><!WA9><!WA9><!WA9><a href="http://www.cs.cornell.edu/Info/People/tah/temporal_proof_methodologies_for_timed_transition_systems.html">
Abstract.</a>
Ftp
<!WA10><!WA10><!WA10><!WA10><a href="ftp://ftp.cs.cornell.edu/pub/tah/Papers/temporal_proof_methodologies_for_timed_transition_systems.ps">
postscript.</a>
<p>
<li>Thomas A. Henzinger, Zohar Manna, and Amir Pnueli.
<b>What good are digital clocks?</b>
<i>Proceedings of the 
19th International Colloquium on Automata, Languages, and Programming</i>
(ICALP 1992),
Lecture Notes in Computer Science 623,
Springer-Verlag, 1992, pp. 545-558.
<!WA11><!WA11><!WA11><!WA11><a href="http://www.cs.cornell.edu/Info/People/tah/what_good_are_digital_clocks.html">
Abstract.</a>
Ftp
<!WA12><!WA12><!WA12><!WA12><a href="ftp://ftp.cs.cornell.edu/pub/tah/Papers/what_good_are_digital_clocks.ps">
postscript.</a>
<p>
<li>Rajeev Alur, Tomas Feder, and Thomas A. Henzinger.
<b>The benefits of relaxing punctuality.</b>
<i>Proceedings of the 
Tenth Annual ACM Symposium on Principles of Distributed Computing</i>
(PODC 1991), pp. 139-152.
<!WA13><!WA13><!WA13><!WA13><a href="http://www.cs.cornell.edu/Info/People/tah/the_benefits_of_relaxing_punctuality.html">
Abstract.</a>
Ftp
<!WA14><!WA14><!WA14><!WA14><a href="ftp://ftp.cs.cornell.edu/pub/tah/Papers/the_benefits_of_relaxing_punctuality.ps">
postscript.</a>
<p>
<li>Thomas A. Henzinger.
<b>Sooner is safer than later.</b>
<i>Information Processing Letters</i> 43:135-141, 1992.                  
<!WA15><!WA15><!WA15><!WA15><a href="http://www.cs.cornell.edu/Info/People/tah/sooner_is_safer_than_later.html">
Abstract.</a>
</ul>
<h3><a name="clock_systems">Clock Systems and Timed Automata</a></h3>
<ul>
<li>Rajeev Alur and Thomas A. Henzinger.
<b>Real-time system = discrete system + clock variables.</b>
In 
<i>Theories and Experiences for Real-time System Development</i>
(T. Rus, C. Rattray, eds.),
AMAST Series in Computing 2,
World Scientific, 1994, pp. 1-29.
<!WA16><!WA16><!WA16><!WA16><a href="http://www.cs.cornell.edu/Info/People/tah/real-time_system=discrete_system+clock_variables.html">
Abstract.</a>
Ftp
<!WA17><!WA17><!WA17><!WA17><a href="ftp://ftp.cs.cornell.edu/pub/tah/Papers/real-time_system=discrete_system+clock_variables.ps">
postscript.</a>
<p>
<li>Thomas A. Henzinger and Peter Kopke.
<b>Verification methods for the divergent runs of clock systems.</b>
<i>Proceedings of the 
Third International Symposium on Formal Techniques in Real-time and 
Fault-tolerant Systems</i>
(FTRTFT 1994), 
Lecture Notes in Computer Science 863,
Springer-Verlag, 1993, pp. 351-372.
<p>
<li>Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine.
<b>Symbolic model checking for real-time systems.</b>
<i>Information and Computation</i> 111:193-244, 1994.
A preliminary version appeared in the 
<i>Proceedings of the 
Seventh Annual IEEE Symposium on Logic in Computer Science</i>
(LICS 1992), pp. 394-406.
<!WA18><!WA18><!WA18><!WA18><a href="http://www.cs.cornell.edu/Info/People/tah/symbolic_model_checking_for_real-time_systems.html">
Abstract.</a>
Ftp
<!WA19><!WA19><!WA19><!WA19><a href="ftp://ftp.cs.cornell.edu/pub/tah/Papers/symbolic_model_checking_for_real-time_systems.ps">
postscript.</a>
<p>
<li>Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi.
<b>Parametric real-time reasoning.</b>
<i>Proceedings of the 
25th Annual ACM Symposium on Theory of Computing</i>
(STOC 1993), pp. 592-601.
<!WA20><!WA20><!WA20><!WA20><a href="http://www.cs.cornell.edu/Info/People/tah/parametric_real-time_reasoning.html">
Abstract.</a>
Ftp
<!WA21><!WA21><!WA21><!WA21><a href="ftp://ftp.cs.cornell.edu/pub/tah/Papers/parametric_real-time_reasoning.ps">
postscript.</a>
<p>
<li>Rajeev Alur, Costas Courcoubetis, and Thomas A. Henzinger. 
<b>Computing accumulated delays in real-time systems.</b>
<i>Proceedings of the 
Fifth International Conference on Computer-aided Verification</i>
(CAV 1993),
Lecture Notes in Computer Science 697,
Springer-Verlag, 1993, pp. 181-193.
<!WA22><!WA22><!WA22><!WA22><a href="http://www.cs.cornell.edu/Info/People/tah/computing_accumulated_delays_in_real-time_systems.html">
Abstract.</a>
Ftp
<!WA23><!WA23><!WA23><!WA23><a href="ftp://ftp.cs.cornell.edu/pub/tah/Papers/computing_accumulated_delays_in_real-time_systems.ps">
postscript.</a>
<p>
<li>Thomas A. Henzinger, Peter Kopke, and Howard Wong-Toi.
<b>The expressive power of clocks.</b>
<i>Proceedings of the 
22nd International Colloquium on Automata, Languages, and Programming</i>
(ICALP 1995),
Lecture Notes in Computer Science 944,
Springer-Verlag, 1995, pp. 417-428.
<p>
<li>Rajeev Alur, Costas Courcoubetis, and Thomas A. Henzinger.
<b>The observational power of clocks.</b>
<i>Proceedings of the 
Fifth International Conference on Concurrency Theory</i>
(CONCUR 1994),
Lecture Notes in Computer Science 836,
Springer-Verlag, 1994, pp. 162-177.
<!WA24><!WA24><!WA24><!WA24><a href="http://www.cs.cornell.edu/Info/People/tah/the_observational_power_of_clocks.html">
Abstract.</a>
Ftp
<!WA25><!WA25><!WA25><!WA25><a href="ftp://ftp.cs.cornell.edu/pub/tah/Papers/the_observational_power_of_clocks.ps">
postscript.</a>
<p>
<li>Rajeev Alur and Thomas A. Henzinger.
<b>Back to the future: towards a theory of timed regular languages.</b>
<i>Proceedings of the 
33rd Annual IEEE Symposium on Foundations of Computer Science</i>
(FOCS 1992), pp. 177-186.
<!WA26><!WA26><!WA26><!WA26><a href="http://www.cs.cornell.edu/Info/People/tah/back_to_the_future.html">
Abstract.</a>
Ftp
<!WA27><!WA27><!WA27><!WA27><a href="ftp://ftp.cs.cornell.edu/pub/tah/Papers/back_to_the_future.ps">
postscript.</a>
<p>
<li>Rajeev Alur, Limor Fix, and Thomas A. Henzinger. 
<b>A determinizable class of timed automata.</b>
<i>Proceedings of the 
Sixth International Conference on Computer-aided Verification</i>
(CAV 1994),
Lecture Notes in Computer Science 818,
Springer-Verlag, 1994, pp. 1-13.
</ul>
<h3><a name="hybrid_automata">Hybrid Automata</a></h3>
<ul>
<li>Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, and Pei-Hsin Ho.
<b>Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems.</b>
In 
<i>Hybrid Systems I</i>,
Lecture Notes in Computer Science 736,
Springer-Verlag, 1993, pp. 209-229.
<!WA28><!WA28><!WA28><!WA28><a href="http://www.cs.cornell.edu/Info/People/tah/hybrid_automata.html">
Abstract.</a>
Ftp
<!WA29><!WA29><!WA29><!WA29><a href="ftp://ftp.cs.cornell.edu/pub/tah/Papers/hybrid_automata.ps">
postscript.</a>
<p>
<li>Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, Nicolas Halbwachs,
Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and 
Sergio Yovine.
<b>The algorithmic analysis of hybrid systems.</b>
<i>Theoretical Computer Science</i> 138:3-34, 1995.
A preliminary version appeared in the 
<i>Proceedings of the 11th International
Conference on Analysis and Optimization of Systems: Discrete-event Systems</i>,
Lecture Notes in Control and Information Sciences 199,
Springer-Verlag, 1994, pp. 331-351.
<!WA30><!WA30><!WA30><!WA30><a href="http://www.cs.cornell.edu/Info/People/tah/the_algorithmic_analysis_of_hybrid_systems.html">
Abstract.</a>
Ftp
<!WA31><!WA31><!WA31><!WA31><a href="ftp://ftp.cs.cornell.edu/pub/tah/Papers/the_algorithmic_analysis_of_hybrid_systems.ps">
postscript.</a>
<p>
<li>Rajeev Alur, Thomas A. Henzinger, and Pei-Hsin Ho.
<b>Automatic symbolic verification of embedded systems.</b>
<i>Proceedings of the 
14th Annual IEEE Real-time Systems Symposium</i>
(RTSS 1993), pp. 2-11.
<!WA32><!WA32><!WA32><!WA32><a href="http://www.cs.cornell.edu/Info/People/tah/automatic_symbolic_verification_of_embedded_systems.html">
Abstract.</a>
Ftp
<!WA33><!WA33><!WA33><!WA33><a href="ftp://ftp.cs.cornell.edu/pub/tah/Papers/automatic_symbolic_verification_of_embedded_systems.ps">
postscript.</a>
<p>
<li>Thomas A. Henzinger and Pei-Hsin Ho.
<b>A note on abstract-interpretation strategies for hybrid automata.</b>
In
<i>Hybrid Systems II</i>,
Lecture Notes in Computer Science 999,
Springer-Verlag, 1995, pp. 252-264.
<!WA34><!WA34><!WA34><!WA34><a href="http://www.cs.cornell.edu/Info/People/tah/model-checking_strategies_for_linear_hybrid_systems.html">
Abstract.</a>
Ftp
<!WA35><!WA35><!WA35><!WA35><a href="ftp://ftp.cs.cornell.edu/pub/tah/Papers/model-checking_strategies_for_linear_hybrid_systems.ps">
postscript.</a>
<p>
<li>Thomas A. Henzinger and Pei-Hsin Ho.
<b>HyTech: The Cornell HYbrid TECHnology Tool.</b>
In
<i>Hybrid Systems II</i>,
Lecture Notes in Computer Science 999,
Springer-Verlag, 1995, pp. 265-294.
<p>
<li>Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi,
<b>HyTech: The Next Generation.</b>
<i>Proceedings of the 
16th Annual IEEE Real-time Systems Symposium</i>
(RTSS 1995), pp. 56-65.
<p>
<li>Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi.
<b>A user guide to HyTech.</b>
<i>Proceedings of the 
First Workshop on Tools and Algorithms for the Construction and Analysis of 
Systems</i>
(TACAS 1995),
Lecture Notes in Computer Science 1019,
Springer-Verlag, 1995, pp. 41-71.
Full version available as Cornell Technical Report CSD-TR-95-1532, 1995.
<p>
<li>Thomas A. Henzinger, Peter Kopke, Anuj Puri, and Pravin Varaiya.
<b>What's decidable about hybrid automata?</b>
<i>Proceedings of the 
27th Annual ACM Symposium on Theory of Computing</i>
(STOC 1995), pp. 373-382.
<p>
<li>Thomas A. Henzinger.
<b>Hybrid automata with finite bisimulations.</b>
<i>Proceedings of the 
22nd International Colloquium on Automata, Languages, and Programming</i>
(ICALP 1995),
Lecture Notes in Computer Science 944,
Springer-Verlag, 1995, pp. 324-335.
<p>
<li>Thomas A. Henzinger and Pei-Hsin Ho.
<b>Algorithmic analysis of nonlinear hybrid systems.</b>
<i>Proceedings of the 
Seventh International Conference on Computer-aided Verification</i>
(CAV 1995),
Lecture Notes in Computer Science 939,
Springer-Verlag, 1995, pp. 225-238.
<p>
<li>Thomas A. Henzinger, Zohar Manna, and Amir Pnueli.
<b>Towards refining temporal specifications into hybrid systems.</b>
In
<i>Hybrid Systems I</i>,
Lecture Notes in Computer Science 736,
Springer-Verlag, 1993, pp. 60-76.
<!WA36><!WA36><!WA36><!WA36><a href="http://www.cs.cornell.edu/Info/People/tah/towards_refining_temporal_specifications_into_hybrid_systems.html">
Abstract.</a>
Ftp
<!WA37><!WA37><!WA37><!WA37><a href="ftp://ftp.cs.cornell.edu/pub/tah/Papers/towards_refining_temporal_specifications_into_hybrid_systems.ps">
postscript.</a>
<p>
<li>Arjun Kapur, Thomas A. Henzinger, Zohar Manna, and Amir Pnueli.
<b>Proving safety properties of hybrid systems.</b>
<i>Proceedings of the 
Third International Symposium on Formal Techniques in Real-time and 
Fault-tolerant Systems</i>
(FTRTFT 1994), 
Lecture Notes in Computer Science 863,
Springer-Verlag, 1993, pp. 431-454.
</ul>
<i>Last updated on September 1, 1995.<br>
tah@cs.cornell.edu</i>

